Formalizing 100 theorems in Coq